$x$ when $e$ $\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$(state when $e$).$x$